COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00011 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.EVERY HEADING(Flow Chart Functions,%8Draft%1,{DATE})
.CB FUNCTIONS CHARACTERIZING FLOW CHARTS


	When one  studies programs organized  as flow charts,  one is
inclined to prefer flow charts with a single entry and a single exit.
However, the operations of building flow charts from parts inevitably
involve flow charts with multiple entries and ultiple exits.

	Our  approach  is  to  characterize flow  charts  by  certain
functions  and show how to get  the functions characterizing new flow
charts from those characterizing  the flow charts from which  the new
ones are formed.   This is in contrast with  the approach of Ianov as
described in (Ianov 1959)  and (Rutledge 1964).   Our reason is  that
mathematics  provides  us   with  powerful  tools   for  manipulating
functions,  and, moreover, facts  about flow charts  must be combined
with other mathematical facts which are most conveniently decribed in
terms of functions, predicates and sets.

.bb "#. Flow chart functions"

	Figure 1 represents  a flow chart ⊗c whose  inner workings we
do not wish to specify, but whose behavior we wish to characterize by
functions.   The arrows into  the ⊗blob  represent paths along  which
control enters  the flow chart  (called entries), and  the arrows out
represent paths  by which  control leaves  it (called  ⊗exits).   Let
⊗En(c) be  the set of  entries of ⊗c,  and let ⊗Ex(c)  be its  set of
exits.   Let ⊗x represent  the state vector, i.e.   the collection of
assignments of values to the variables occurring in the program.   We
define predicates  %2p%4ij⊗(x,c) where ⊗i  ranges over ⊗En(c)  and ⊗j
ranges over  ⊗Ex(c), and functions %2s%4i⊗(x,c) where ⊗i again ranges
over ⊗En(c) as follows:

	(i) %2p%4ij⊗(x,c) is  true if and  only if entering the  flow
chart ⊗c  at entry ⊗i  with initial state  ⊗x results in  leaving the
flow chart at exit ⊗j.

	(ii) %2s%4i⊗(x,c) is the value of the state at exit from  the
flow chart when it is entered at ⊗i with initial state ⊗x.  Note that
⊗s is a partial functions, because the program may never exit.

	Obviously the predicates %2p%4ij%1 and the functions %2s%4i%1
characterize the flow chart ⊗c, because if one knows these  one knows
where the program  will exit and what  the new state will  be for any
entrance into the flow chart.

	If  we suppose that the flow  chart is ultimately constructed
out of elementary compute blocks and elementary  decision blocks, one
needs to show how to write the %2p%1's and %2s%1's for these elements
and then  how to  get the  %2p%1's and  %2s%1's for  a combination  of
blocks from  those of  its  parts.   The first  part is  trivial.   A
compute block  has just one entry and one exit,  so there is just one
⊗p and it is identically  true, and there is  just one ⊗s, and it  is
just the  function of tate computed  by the block.   A decision block
has one  entry and two exits and the one ⊗p is just the predicate for
the YES decision and the other is the predicate  for the NO decision.
There is one ⊗s, and it is the identity function.

	We use the following operations that give new charts from old
ones.

	(i) Suppression of an entry %2i%40%1  from a chart ⊗c.   This
gives a new chart  %2del(c,i%40%2)%1 with one fewer entry,  and whose
%2p%1's and %2s%1's  are the same as before except that the subscript
%2i%40%1 is omitted.

	(ii) Putting two charts ⊗c1 and  ⊗c2 side by side.  Call  the
new  chart %2c1∪ε2%1.   We  have %2En(c1∪c2)  = En(c1)∪En(c2)%1,  and
%2Ex(c1∪c2) = Ex(c1) ∪ Ex(c2)%1.  Moreover, we have

	%2p%4ij%2(x,c1∪c2)  = %3if%2 i  ε c1 %3then%2 (%3if%2  j ε c1
%3then%2 p%4ij%2(x,c1) %3else false)  else (if%2 j ε c1  %3then false
else %2p%4ij%2(x,c2))%1,

and

	%2s%4i%2(x,c1∪c2)  =  %3if%2  i  ε c1  %3then%2  s%4i%2(x,c1)
%3else%2 p%4i%2(x,c2)%1.

Both of these are trivial operations but the next is not.

	(iii) Connecting  the exit  ⊗m  to the  entry  ⊗n
giving a  new chart  %2loop(c,m,n)%1 with  one fewer  exit.
The new %2p%1's and %2s%1's are defined by the recursion equations
	%2p%4ij%2(x,loop(c,m,n)) ← %3if%2 p%4in%2(x,c) %3then%2
p%4mj%2(s'(s%4i%2(x,c),c,m,n),c) %3else%2 p%4ij%2(x,c)%1,

and

	%2s%4i%2(x,loop(c,m,n)) ← %3if%2 p%4in%2(x,c) %3then%2
s%4m%2(s'(s%4i%2(x,c),c,m,n),c) %3else%2 s%4i%2(x,c)%1,

where

	%2s'(x,c,m,n) ← %3if%2 p%4mn%2(x,c) %3then%2 s'(s%4m%2(x,c),c,m,n)
%3else%2 x%1.

	A little contemplation will show that this recursive process
captures our intuitive notion of what happens when an exit is connected
to an entry.  If we were using another formal notion of the computation
performed by a flow chart, then we would have to prove theorems in
order to justify (i) - (iii).

	An objective worth undertaking is to show that any two equivalent
flow charts can be proved equivalent by the theory of recursively
defined functions from these definitions.  This would be the analog
of Ianov's theorem and ought to be based on a decision procedure for
recursions (possibly restricted to iterative form) where there is only
one variable.
It would have the advantage over the Ianov theory that it is simply
the theory of recursion equations applied to this case rather than
an ad hoc confection.

	I don't know such a decision procedure, nor has there been
formulated a theory of recursion equations that is proved complete
for this case.